(define tableau
   {valid --> valid}
    Valid -> Valid   where (empty? Valid)
    Valid -> (let Literals (fix (fn vl) Valid)
                  AllValid (contradiction$ true Literals)
                  (if (empty? AllValid)
                      Valid
                      (try-all-valid AllValid Valid))))

(define try-all-valid
    {(list valid) --> valid --> valid}
     [ ] Valid -> Valid
     [Valid | _] _ -> Valid   where (empty? Valid)
     [Valid |  AllValid] Valid ->  (let TryHead (tableau Valid)
                                        (if (empty? TryHead)
                                            TryHead
                                            (try-all-valid AllValid Valid))))
